Step of Proof: mu'_wf 11,40
Inference at * 2 
Iof proof for Lemma mu' wf:



1. A : Type
2. P : A
3. d : x:A. Dec(n:. ((P(x,n))))
  (x.(TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1)  A( + Top) 
latex
 by Auto 
latex

 .

Definitionsx.A(x), t.1, x. t(x), p-mu-decider, , Type, Dec(P), b, P  Q, x:AB(x), left + right, , Top, x:A. B(x), x:A  B(x), p-mu(P;x), x:A. B(x), f(a), t  T
Lemmaspi1 wf, p-mu-decider, bool wf, top wf, decidable wf, nat wf, assert wf, p-mu wf

origin